Step of Proof: decidable__implies_better 11,40

Inference at * 1 1 1 
Iof proof for Lemma decidable implies better:



1. P : 
2. Q : x:P.
3. P
4. P  Dec(Q)
  (P  Q ((P  Q)) 
latex

 by ThinTrivial 
THEN Assert Q   
latex


TH1: .....assertion..... NILNIL

TH1: 4. Dec(Q)
TH1:   Q  
TH2

TH2: 4. Dec(Q)
TH2: 5. Q  
TH2:   (P  Q ((P  Q))
TH.


Definitionst  T, , P  Q

origin